discrete\_struct\{i:l\}($A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it sort}$:($A$$\rightarrow$Type$_{\mbox{\scriptsize i}}$)$\times$($a$:$A$$\rightarrow$EqDecider(${\it sort}$($a$)))